1 /-
2 Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Zhouhang Zhou
5 -/
6
7 import analysis.convex.basic algebra.quadratic_discriminant analysis.complex.exponential
src └───────────────────┘ └────────────────────────────┘ └──────────────────────────┘
8 analysis.specific_limits
src └──────────────────────┘
9 import tactic.monotonicity
src └─────────────────┘
10
11
12 /-!
13 # Inner Product Space
14
15 This file defines real inner product space and proves its basic properties.
16
17 An inner product space is a vector space endowed with an inner product. It generalizes the notion of
18 dot product in `ℝ^n` and provides the means of defining the length of a vector and the angle between
19 two vectors. In particular vectors `x` and `y` are orthogonal if their inner product equals zero.
20
21 ## Main statements
22
23 Existence of orthogonal projection onto nonempty complete subspace:
24 Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace.
25 Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
26 The point `v` is usually called the orthogonal projection of `u` onto `K`.
27
28 ## Implementation notes
29
30 We decide to develop the theory of real inner product spaces and that of complex inner product
31 spaces separately.
32
33 ## Tags
34
35 inner product space, norm, orthogonal projection
36
37 ## References
38 * [Clément & Martin, *The Lax-Milgram Theorem. A detailed proof to be formalized in Coq*]
39 * [Clément & Martin, *A Coq formal proof of the Lax–Milgram theorem*]
40
41 The Coq code is available at the following address: <http://www.lri.fr/~sboldo/elfic/index.html>
42 -/
43
44 noncomputable theory
45
46 open real set lattice
47 open_locale topological_space
48
49 universes u v w
50
51 variables {α : Type u} {F : Type v} {G : Type w}
52
53 set_option class.instance_max_depth 40
doc └──────────────────────┘
54
55 class has_inner (α : Type*) := (inner : α → α → ℝ)
id └───┘ ┴ ┴ ┴ ┴
src ┴
typ └───┘ ┴ ┴ ┴ ┴
56
57 export has_inner (inner)
58
59 section prio
60 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
61 -- see Note[vector space definition] for why we extend `module`.
62 /--
63 An inner product space is a real vector space with an additional operation called inner product.
64 Inner product spaces over complex vector space will be defined in another file.
65 -/
66 class inner_product_space (α : Type*) extends add_comm_group α, module ℝ α, has_inner α :=
67 (comm : ∀ x y, inner x y = inner y x)
68 (nonneg : ∀ x, 0 ≤ inner x x)
69 (definite : ∀ x, inner x x = 0 → x = 0)
70 (add_left : ∀ x y z, inner (x + y) z = inner x z + inner y z)
71 (smul_left : ∀ x y r, inner (r • x) y = r * inner x y)
72 end prio
73
74 variable [inner_product_space α]
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
75
76 section basic_properties
77
78 lemma inner_comm (x y : α) : inner x y = inner y x := inner_product_space.comm x y
id ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──────────────────────┘ ┴ ┴
src └───┘ ┴ └───┘ └──────────────────────┘
typ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──────────────────────┘ ┴ ┴
79
80 lemma inner_self_nonneg {x : α} : 0 ≤ inner x x := inner_product_space.nonneg _
id ┴ ┴ └───┘ ┴ ┴ └────────────────────────┘
src ┴ └───┘ └────────────────────────┘
typ ┴ ┴ └───┘ ┴ ┴ └────────────────────────┘
81
82 lemma inner_add_left {x y z : α} : inner (x + y) z = inner x z + inner y z :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
83 inner_product_space.add_left _ _ _
id └──────────────────────────┘
src └──────────────────────────┘
typ └──────────────────────────┘
84
85 lemma inner_add_right {x y z : α} : inner x (y + z) = inner x y + inner x z :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
86 by { rw [inner_comm, inner_add_left], simp [inner_comm] }
id └────────┘ └────────────┘ └────────┘
src └──┘└────────┘└┘└────────────┘┴ └────┘└────────┘└┘
typ └──┘└────────┘└┘└────────────┘┴ └────┘└────────┘└┘
doc └──┘ └┘ ┴ └────┘ └┘
txt └──┘ └┘ ┴ └────┘ └┘
par └──┘ └┘ ┴ └────┘ └┘
pid └┘ └┘ ┴ ┴┴ ┴┴
st └───────────────┘└──────────────┘└───────────────────┘└┘
87
88 lemma inner_smul_left {x y : α} {r : ℝ} : inner (r • x) y = r * inner x y :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ └───┘
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
89 inner_product_space.smul_left _ _ _
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
90
91 lemma inner_smul_right {x y : α} {r : ℝ} : inner x (r • y) = r * inner x y :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ └───┘
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
92 by { rw [inner_comm, inner_smul_left, inner_comm] }
id └────────┘ └─────────────┘ └────────┘
src └──┘└────────┘└┘└─────────────┘└┘└────────┘└┘
typ └──┘└────────┘└┘└─────────────┘└┘└────────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st └───────────────┘└───────────────┘└──────────┘┴┴└┘
93
94 @[simp] lemma inner_zero_left {x : α} : inner 0 x = 0 :=
id ┴ └───┘ ┴ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ ┴
doc └──┘
95 by { rw [← zero_smul ℝ (0:α), inner_smul_left, zero_mul] }
id └───────┘ ┴ └─────────────┘ └──────┘
src └────┘└───────┘┴ ┴ └┘ └─┘└─────────────┘└┘└──────┘└┘
typ └────┘└───────┘┴ ┴ └┘┴└─┘└─────────────┘└┘└──────┘└┘
doc └────┘ ┴ ┴ └┘ └─┘ └┘ └┘
txt └────┘ ┴ ┴ └┘ └─┘ └┘ └┘
par └────┘ ┴ ┴ └┘ └─┘ └┘ └┘
pid └──┘ ┴ ┴ └┘ └─┘ └┘ ┴┴
st └────────────────────────┘└───────────────┘└────────┘┴┴└┘
96
97 @[simp] lemma inner_zero_right {x : α} : inner x 0 = 0 :=
id ┴ └───┘ ┴ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ ┴
doc └──┘
98 by { rw [inner_comm, inner_zero_left] }
id └────────┘ └─────────────┘
src └──┘└────────┘└┘└─────────────┘└┘
typ └──┘└────────┘└┘└─────────────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st └───────────────┘└───────────────┘┴┴└┘
99
100 lemma inner_self_eq_zero (x : α) : inner x x = 0 ↔ x = 0 :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
101 iff.intro (inner_product_space.definite _) (by { rintro rfl, exact inner_zero_left })
id └───────┘ └──────────────────────────┘ └─────────────┘
src └───────┘ └──────────────────────────┘ └────────┘ └────┘└─────────────┘┴
typ └───────┘ └──────────────────────────┘ └────────┘ └────┘└─────────────┘┴
doc └────────┘ └────┘ ┴
txt └────────┘ └────┘ ┴
par └────────┘ └────┘ ┴
pid └──┘ ┴ ┴
st └───────────┘└──────────────────────┘└┘
102
103 @[simp] lemma inner_neg_left {x y : α} : inner (-x) y = -inner x y :=
id ┴ └───┘ ┴┴ ┴ ┴ ┴└───┘ ┴ ┴
src └───┘ ┴ ┴ ┴└───┘
typ ┴ └───┘ ┴┴ ┴ ┴ ┴└───┘ ┴ ┴
doc └──┘
104 by { rw [← neg_one_smul ℝ x, inner_smul_left], simp }
id └──────────┘ ┴ └─────────────┘
src └────┘└──────────┘┴ ┴ └┘└─────────────┘┴ └───┘
typ └────┘└──────────┘┴ ┴┴└┘└─────────────┘┴ └───┘
doc └────┘ ┴ ┴ └┘ ┴ └───┘
txt └────┘ ┴ ┴ └┘ ┴ └───┘
par └────┘ ┴ ┴ └┘ ┴ └───┘
pid └──┘ ┴ ┴ └┘ ┴ ┴
st └───────────────────────┘└───────────────┘└──────┘└┘
105
106 @[simp] lemma inner_neg_right {x y : α} : inner x (-y) = -inner x y :=
id ┴ └───┘ ┴ ┴┴ ┴ ┴└───┘ ┴ ┴
src └───┘ ┴ ┴ ┴└───┘
typ ┴ └───┘ ┴ ┴┴ ┴ ┴└───┘ ┴ ┴
doc └──┘
107 by { rw [inner_comm, inner_neg_left, inner_comm] }
id └────────┘ └────────────┘ └────────┘
src └──┘└────────┘└┘└────────────┘└┘└────────┘└┘
typ └──┘└────────┘└┘└────────────┘└┘└────────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st └───────────────┘└──────────────┘└──────────┘┴┴└┘
108
109 @[simp] lemma inner_neg_neg {x y : α} : inner (-x) (-y) = inner x y := by simp
id ┴ └───┘ ┴┴ ┴┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ ┴ ┴ └───┘ └────
typ ┴ └───┘ ┴┴ ┴┴ ┴ └───┘ ┴ ┴ └────
doc └──┘ └────
txt └────
par └────
pid └
st └─────
110
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
111 lemma inner_sub_left {x y z : α} : inner (x - y) z = inner x z - inner y z :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
112 by { simp [sub_eq_add_neg, inner_add_left] }
id └────────────┘ └────────────┘
src └────┘└────────────┘└┘└────────────┘└┘
typ └────┘└────────────┘└┘└────────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st └───────────────────────────────────────┘└┘
113
114 lemma inner_sub_right {x y z : α} : inner x (y - z) = inner x y - inner x z :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
115 by { simp [sub_eq_add_neg, inner_add_right] }
id └────────────┘ └─────────────┘
src └────┘└────────────┘└┘└─────────────┘└┘
typ └────┘└────────────┘└┘└─────────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st └────────────────────────────────────────┘└┘
116
117 /-- Expand `inner (x + y) (x + y)` -/
118 lemma inner_add_add_self {x y : α} : inner (x + y) (x + y) = inner x x + 2 * inner x y + inner y y :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
119 by { simpa [inner_add_left, inner_add_right, two_mul] using inner_comm _ _ }
id └────────────┘ └─────────────┘ └─────┘ └────────┘
src └─────┘└────────────┘└┘└─────────────┘└┘└─────┘└──────┘└────────┘└───┘
typ └─────┘└────────────┘└┘└─────────────┘└┘└─────┘└──────┘└────────┘└───┘
doc └─────┘ └┘ └┘ └──────┘ └───┘
txt └─────┘ └┘ └┘ └──────┘ └───┘
par └─────┘ └┘ └┘ └──────┘ └───┘
pid ┴┴ └┘ └┘ ┴┴└────┘ └──┘┴
st └───────────────────────────────────────────────────────────────────────┘└┘
120
121 /-- Expand `inner (x - y) (x - y)` -/
122 lemma inner_sub_sub_self {x y : α} : inner (x - y) (x - y) = inner x x - 2 * inner x y + inner y y :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
123 by { simp only [inner_sub_left, inner_sub_right, two_mul], simpa using inner_comm _ _ }
id └────────────┘ └─────────────┘ └─────┘ └────────┘
src └─────────┘└────────────┘└┘└─────────────┘└┘└─────┘┴ └──────────┘└────────┘└───┘
typ └─────────┘└────────────┘└┘└─────────────┘└┘└─────┘┴ └──────────┘└────────┘└───┘
doc └─────────┘ └┘ └┘ ┴ └──────────┘ └───┘
txt └─────────┘ └┘ └┘ ┴ └──────────┘ └───┘
par └─────────┘ └┘ └┘ ┴ └──────────┘ └───┘
pid ┴└──┘└┘ └┘ └┘ ┴ ┴└────┘ └──┘┴
st └─────────────────────────────────────────────────────┘└───────────────────────────┘└┘
124
125 /-- Parallelogram law -/
126 lemma parallelogram_law {x y : α} :
id ┴
typ ┴
127 inner (x + y) (x + y) + inner (x - y) (x - y) = 2 * (inner x x + inner y y) :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ └───┘
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
128 by { simp [inner_add_add_self, inner_sub_sub_self, two_mul] }
id └────────────────┘ └────────────────┘ └─────┘
src └────┘└────────────────┘└┘└────────────────┘└┘└─────┘└┘
typ └────┘└────────────────┘└┘└────────────────┘└┘└─────┘└┘
doc └────┘└────────────────┘└┘└────────────────┘└┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st └────────────────────────────────────────────────────────┘└┘
129
130 /-- Cauchy–Schwarz inequality -/
131 lemma inner_mul_inner_self_le (x y : α) : inner x y * inner x y ≤ inner x x * inner y y :=
id ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───┘ ┴ └───┘ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
132 begin
st └─────
133 have : ∀ t, 0 ≤ inner y y * t * t + 2 * inner x y * t + inner x x, from
id ┴ ┴ ┴ ┴ └───┘ ┴
src └─────┘ └┘ └─┘┴┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘┴ ┴ └────
typ └─────┘ └┘ └─┘┴┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴└─┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴└───┘┴ ┴┴ └────
doc └─────┘ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
txt └─────┘ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
par └─────┘ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
pid └───┘└┘ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
st ──────────────────────────────────────────────────────────────────┘└──────
134 assume t, calc
src ───┘ └──┘ └
typ ───┘ └──┘ └
doc ───┘ └──┘ └
txt ───┘ └──┘ └
par ───┘ └──┘ └
pid ───┘ └──┘ └
st ───────────────────
135 0 ≤ inner (x+t•y) (x+t•y) : inner_self_nonneg
id ┴ └───────────────┘
src ───────┘ ┴ ┴ ┴ └┘ └──┘└───────────────┘└
typ ───────┘ ┴ ┴ ┴ └┘ └──┘└───────────────┘└
doc ───────┘ ┴ ┴ └┘ └──┘ └
txt ───────┘ ┴ ┴ └┘ └──┘ └
par ───────┘ ┴ ┴ └┘ └──┘ └
pid ───────┘ ┴ ┴ └┘ └──┘ └
st ────────────────────────────────────────────────────
136 ... = inner y y * t * t + 2 * inner x y * t + inner x x :
id ┴ └───┘ ┴
src ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘┴ ┴ └──
typ ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴└───┘┴ ┴┴└──
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ────────────────────────────────────────────────────────────────
137 by { simp only [inner_add_add_self, inner_smul_right, inner_smul_left], ring },
id └────────────────┘ └──────────────┘ └─────────────┘
src ───────┘ └─┘└─────────┘└────────────────┘└┘└──────────────┘└┘└─────────────┘┴└┘└───┘┴
typ ───────┘ └─┘└─────────┘└────────────────┘└┘└──────────────┘└┘└─────────────┘┴└┘└───┘┴
doc ───────┘ └─┘└─────────┘└────────────────┘└┘ └┘ ┴└┘└───┘┴
txt ───────┘ └─┘└─────────┘ └┘ └┘ ┴└┘└───┘┴
par ───────┘ └─┘└─────────┘ └┘ └┘ ┴└┘└───┘┴
pid ───────┘ └────────────┘ └┘ └┘ └───────┘
st ─────────┘└──────────────────────────────────────────────────────────────────┘└─────┘└┘└
138 have := discriminant_le_zero this, rw discrim at this,
id └──────────────────┘ └──┘ └─────┘
src └──────┘└──────────────────┘┴ └─┘└─────┘└──────┘
typ └──────┘└──────────────────┘┴└──┘ └─┘└─────┘└──────┘
doc └──────┘└──────────────────┘┴ └─┘└─────┘└──────┘
txt └──────┘ ┴ └─┘ └──────┘
par └──────┘ ┴ └─┘ └──────┘
pid └───┘└─┘ ┴ ┴ └──────┘
st ──────────────────────────────────┘└──────────────────┘└─
139 have h : (2 * inner x y)^2 - 4 * inner y y * inner x x =
id ┴ ┴ ┴
src └───────┘ └┘ ┴ ┴ ┴ ┴┴└┘┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴└
typ └───────┘ └┘ ┴ ┴ ┴ ┴┴└┘┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴└
doc └───────┘ └┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
txt └───────┘ └┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par └───────┘ └┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid └────┘└─┘ └┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ───────────────────────────────────────────────────────────
140 4 * (inner x y * inner x y - inner x x * inner y y) := by ring,
id ┴ └───┘ ┴
src ───────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘┴ ┴ └───┘ ┴└──┘
typ ───────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴└───┘┴ ┴┴└───┘ ┴└──┘
doc ───────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘
txt ───────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘
par ───────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└──┘
pid ───────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └───┘
st ──────────────────────────────────────────────────────────────────────────────┘└───┘└─
141 rw h at this,
id ┴
src └─┘ └──────┘
typ └─┘┴└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ─────────────┘└─
142 linarith
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
st ──────────┘
143 end
st └─┘
144
145 end basic_properties
146
147 section norm
148
149 /-- An inner product naturally induces a norm. -/
150 @[priority 100] -- see Note [lower instance priority]
151 instance inner_product_space_has_norm : has_norm α := ⟨λx, sqrt (inner x x)⟩
id └──────┘ ┴ ┴ └──┘ └───┘ ┴ ┴
src └──────┘ └──┘ └───┘
typ └──────┘ ┴ ┴ └──┘ └───┘ ┴ ┴
doc └──────┘
152
153 lemma norm_eq_sqrt_inner {x : α} : ∥x∥ = sqrt (inner x x) := rfl
id ┴ ┴┴┴ ┴ └──┘ └───┘ ┴ ┴ └─┘
src ┴ ┴ ┴ └──┘ └───┘ └─┘
typ ┴ ┴┴┴ ┴ └──┘ └───┘ ┴ ┴ └─┘
154
155 lemma inner_self_eq_norm_square (x : α) : inner x x = ∥x∥ * ∥x∥ := (mul_self_sqrt inner_self_nonneg).symm
id ┴ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ └───────────┘ └───────────────┘ └──┘
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ └───────────────┘ └──┘
typ ┴ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ └───────────┘ └───────────────┘ └──┘
156
157 /-- Expand the square -/
158 lemma norm_add_pow_two {x y : α} : ∥x + y∥^2 = ∥x∥^2 + 2 * inner x y + ∥y∥^2 :=
id ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴┴┴
src ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴ ┴┴
typ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴┴┴
159 by { repeat {rw [pow_two, ← inner_self_eq_norm_square]}, exact inner_add_add_self }
id └─────┘ └───────────────────────┘ └────────────────┘
src └──────┘└──┘└─────┘└──┘└───────────────────────┘┴┴ └────┘└────────────────┘┴
typ └──────┘└──┘└─────┘└──┘└───────────────────────┘┴┴ └────┘└────────────────┘┴
doc └──────┘└──┘ └──┘ ┴┴ └────┘└────────────────┘┴
txt └──────┘└──┘ └──┘ ┴┴ └────┘ ┴
par └──────┘└──┘ └──┘ ┴┴ └────┘ ┴
pid └────┘ └──┘ └┘ ┴ ┴
st └────────────────────┘└───────────────────────────┘└─┘└────────────────────────┘└┘
160
161 /-- Same lemma as above but in a different form -/
162 lemma norm_add_mul_self {x y : α} : ∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + 2 * inner x y + ∥y∥ * ∥y∥ :=
id ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
163 by { repeat {rw [← pow_two]}, exact norm_add_pow_two }
id └─────┘ └──────────────┘
src └──────┘└────┘└─────┘┴┴ └────┘└──────────────┘┴
typ └──────┘└────┘└─────┘┴┴ └────┘└──────────────┘┴
doc └──────┘└────┘ ┴┴ └────┘└──────────────┘┴
txt └──────┘└────┘ ┴┴ └────┘ ┴
par └──────┘└────┘ ┴┴ └────┘ ┴
pid └──────┘ └┘ ┴ ┴
st └──────────────────────┘└─┘└──────────────────────┘└┘
164
165 /-- Expand the square -/
166 lemma norm_sub_pow_two {x y : α} : ∥x - y∥^2 = ∥x∥^2 - 2 * inner x y + ∥y∥^2 :=
id ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴┴┴
src ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ └───┘ ┴ ┴ ┴┴
typ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴┴┴
167 by { repeat {rw [pow_two, ← inner_self_eq_norm_square]}, exact inner_sub_sub_self }
id └─────┘ └───────────────────────┘ └────────────────┘
src └──────┘└──┘└─────┘└──┘└───────────────────────┘┴┴ └────┘└────────────────┘┴
typ └──────┘└──┘└─────┘└──┘└───────────────────────┘┴┴ └────┘└────────────────┘┴
doc └──────┘└──┘ └──┘ ┴┴ └────┘└────────────────┘┴
txt └──────┘└──┘ └──┘ ┴┴ └────┘ ┴
par └──────┘└──┘ └──┘ ┴┴ └────┘ ┴
pid └────┘ └──┘ └┘ ┴ ┴
st └────────────────────┘└───────────────────────────┘└─┘└────────────────────────┘└┘
168
169 /-- Same lemma as above but in a different form -/
170 lemma norm_sub_mul_self {x y : α} : ∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ - 2 * inner x y + ∥y∥ * ∥y∥ :=
id ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
171 by { repeat {rw [← pow_two]}, exact norm_sub_pow_two }
id └─────┘ └──────────────┘
src └──────┘└────┘└─────┘┴┴ └────┘└──────────────┘┴
typ └──────┘└────┘└─────┘┴┴ └────┘└──────────────┘┴
doc └──────┘└────┘ ┴┴ └────┘└──────────────┘┴
txt └──────┘└────┘ ┴┴ └────┘ ┴
par └──────┘└────┘ ┴┴ └────┘ ┴
pid └──────┘ └┘ ┴ ┴
st └──────────────────────┘└─┘└──────────────────────┘└┘
172
173 /-- Cauchy–Schwarz inequality with norm -/
174 lemma abs_inner_le_norm (x y : α) : abs (inner x y) ≤ ∥x∥ * ∥y∥ :=
id ┴ └─┘ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
src └─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
175 nonneg_le_nonneg_of_squares_le (mul_nonneg (sqrt_nonneg _) (sqrt_nonneg _))
id └────────────────────────────┘ └────────┘ └─────────┘ └─────────┘
src └────────────────────────────┘ └────────┘ └─────────┘ └─────────┘
typ └────────────────────────────┘ └────────┘ └─────────┘ └─────────┘
176 begin
st └─────
177 rw abs_mul_abs_self,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
178 have : ∥x∥ * ∥y∥ * (∥x∥ * ∥y∥) = inner x x * inner y y,
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴
src └─────┘┴ ┴┴┴┴ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴ ┴ ┴└───┘┴ ┴
typ └─────┘┴ ┴┴┴┴ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴┴┴ ┴└───┘┴ ┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
179 simp only [inner_self_eq_norm_square], ring,
id └───────────────────────┘
src └─────────┘└───────────────────────┘┴ └──┘
typ └─────────┘└───────────────────────┘┴ └──┘
doc └─────────┘ ┴ └──┘
txt └─────────┘ ┴ └──┘
par └─────────┘ ┴ └──┘
pid ┴└──┘└┘ ┴
st ────────────────────────────────────────┘└────┘└─
180 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
181 exact inner_mul_inner_self_le _ _
id └─────────────────────┘
src └────┘└─────────────────────┘└───┘
typ └────┘└─────────────────────┘└───┘
doc └────┘└─────────────────────┘└───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └──┘┴
st ───────────────────────────────────┘
182 end
st └─┘
183
184 lemma parallelogram_law_with_norm {x y : α} :
id ┴
typ ┴
185 ∥x + y∥ * ∥x + y∥ + ∥x - y∥ * ∥x - y∥ = 2 * (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥) :=
id ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴
186 by { simp only [(inner_self_eq_norm_square _).symm], exact parallelogram_law }
id └───────────────────────┘ └───────────────┘
src └─────────┘ └───────────────────────┘└───────┘ └────┘└───────────────┘┴
typ └─────────┘ └───────────────────────┘└───────┘ └────┘└───────────────┘┴
doc └─────────┘ └───────┘ └────┘└───────────────┘┴
txt └─────────┘ └───────┘ └────┘ ┴
par └─────────┘ └───────┘ └────┘ ┴
pid ┴└──┘└┘ └───────┘ ┴ ┴
st └───────────────────────────────────────────────┘└────────────────────────┘└┘
187
188 /-- An inner product space forms a normed group w.r.t. its associated norm. -/
189 @[priority 100] -- see Note [lower instance priority]
190 instance inner_product_space_is_normed_group : normed_group α :=
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──────────┘
191 normed_group.of_core α
id └──────────────────┘ ┴
src └──────────────────┘
typ └──────────────────┘ ┴
doc └──────────────────┘
192 { norm_eq_zero_iff := assume x, iff.intro
id ┴ └───────┘
src └───────┘
typ ┴ └───────┘
193 (λ h : sqrt (inner x x) = 0, (inner_self_eq_zero x).1 $ (sqrt_eq_zero inner_self_nonneg).1 h )
id └──┘ └───┘ ┴ ┴ ┴ └────────────────┘ ┴ ┴ └──────────┘ └───────────────┘ ┴ ┴
src └──┘ └───┘ ┴ └────────────────┘ ┴ └──────────┘ └───────────────┘ ┴
typ └──┘ └───┘ ┴ ┴ ┴ └────────────────┘ ┴ ┴ └──────────┘ └───────────────┘ ┴ ┴
194 (by {rintro rfl, show sqrt (inner (0:α) 0) = 0, simp }),
id └──┘ └───┘ ┴ ┴
src └────────┘ └───┘└──┘┴ └───┘┴ └┘ └───┘┴└┘ └───┘
typ └────────┘ └───┘└──┘┴ └───┘┴ └┘┴└───┘┴└┘ └───┘
doc └────────┘ └───┘ ┴ ┴ └┘ └───┘ └┘ └───┘
txt └────────┘ └───┘ ┴ ┴ └┘ └───┘ └┘ └───┘
par └────────┘ └───┘ ┴ ┴ └┘ └───┘ └┘ └───┘
pid └──┘ └───┘ ┴ ┴ └┘ └───┘ ┴┴ ┴
st └──────────┘└─────────────────────────────┘└─────┘└┘
195 triangle := assume x y,
id ┴ ┴
typ ┴ ┴
196 begin
st └─────
197 have := calc
src └──────┘ └
typ └──────┘ └
doc └──────┘ └
txt └──────┘ └
par └──────┘ └
pid └───┘└─┘ └
st ─────────────────
198 ∥x + y∥ * ∥x + y∥ = inner (x + y) (x + y) : (inner_self_eq_norm_square _).symm
id ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───────────────────────┘
src ─────┘┴ ┴┴┴ ┴┴┴┴ ┴ ┴ ┴ ┴└───┘┴ ┴ ┴ └┘ ┴ ┴ └──┘ └───────────────────────┘└────────
typ ─────┘┴ ┴┴┴ ┴┴┴┴ ┴ ┴ ┴ ┴└───┘┴ ┴ ┴ └┘ ┴┴ ┴┴└──┘ └───────────────────────┘└────────
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ └────────
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ └────────
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ └────────
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ └────────
st ─────────────────────────────────────────────────────────────────────────────────────
199 ... = inner x x + 2 * inner x y + inner y y : inner_add_add_self
id └────────────────┘
src ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└────────────────┘└
typ ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└────────────────┘└
doc ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└────────────────┘└
txt ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ───────────────────────────────────────────────────────────────────────
200 ... ≤ inner x x + 2 * (∥x∥ * ∥y∥) + inner y y :
src ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
typ ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
doc ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
txt ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
par ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
pid ─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────────────
201 by linarith [abs_inner_le_norm x y, le_abs_self (inner x y)]
id └───────────────┘ ┴ ┴ └─────────┘ └───┘ ┴ ┴
src ───────┘ ┴└────────┘└───────────────┘┴ ┴ └┘└─────────┘┴ └───┘┴ ┴ └──
typ ───────┘ ┴└────────┘└───────────────┘┴┴┴┴└┘└─────────┘┴ └───┘┴┴┴┴└──
doc ───────┘ ┴└────────┘└───────────────┘┴ ┴ └┘ ┴ ┴ ┴ └──
txt ───────┘ ┴└────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──
par ───────┘ ┴└────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──
pid ───────┘ └─────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──
st ─────────┘└──────────────────────────────────────────────────────────
202 ... = (∥x∥ + ∥y∥) * (∥x∥ + ∥y∥) : by { simp only [inner_self_eq_norm_square], ring },
id └───────────────────────┘
src ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └─┘└─────────┘└───────────────────────┘┴└┘└───┘┴
typ ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └─┘└─────────┘└───────────────────────┘┴└┘└───┘┴
doc ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └─┘└─────────┘ ┴└┘└───┘┴
txt ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └─┘└─────────┘ ┴└┘└───┘┴
par ─────┘└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └─┘└─────────┘ ┴└┘└───┘┴
pid ─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └────────────┘ └───────┘
st ─────┘└──────────────────────────────────┘└──────────────────────────────────────┘└─────┘└┘└
203 exact nonneg_le_nonneg_of_squares_le (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this
id └────────────────────────────┘ └────────┘ └─────────┘ └──┘
src └────┘└────────────────────────────┘┴ └────────┘┴ └──┘ └─────────┘└───┘ └
typ └────┘└────────────────────────────┘┴ └────────┘┴ └──┘ └─────────┘└───┘└──┘└
doc └────┘ ┴ ┴ └──┘ └───┘ └
txt └────┘ ┴ ┴ └──┘ └───┘ └
par └────┘ ┴ ┴ └──┘ └───┘ └
pid ┴ ┴ ┴ └──┘ └───┘ └
st ───────────────────────────────────────────────────────────────────────────────────────────
204 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
205 norm_neg := λx, show sqrt (inner (-x) (-x)) = sqrt (inner x x), by simp }
id ┴ └──┘ └───┘ ┴┴ ┴┴ ┴ └──┘ └───┘ ┴ ┴
src └──┘ └───┘ ┴ ┴ ┴ └──┘ └───┘ └───┘
typ ┴ └──┘ └───┘ ┴┴ ┴┴ ┴ └──┘ └───┘ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
206
207 /-- An inner product space forms a normed space over reals w.r.t. its associated norm. -/
208 instance inner_product_space_is_normed_space : normed_space ℝ α :=
id └──────────┘ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴
doc └──────────┘
209 { norm_smul := assume r x,
id ┴ ┴
typ ┴ ┴
210 begin
st └─────
211 rw [norm_eq_sqrt_inner, sqrt_eq_iff_mul_self_eq,
id └────────────────┘ └─────────────────────┘
src └──┘└────────────────┘└┘└─────────────────────┘└─
typ └──┘└────────────────┘└┘└─────────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ └─
st ─────────────────────────┘└───────────────────────┘└─
212 inner_smul_left, inner_smul_right, inner_self_eq_norm_square],
id └─────────────┘ └──────────────┘ └───────────────────────┘
src ───────┘└─────────────┘└┘└──────────────┘└┘└───────────────────────┘┴
typ ───────┘└─────────────┘└┘└──────────────┘└┘└───────────────────────┘┴
doc ───────┘ └┘ └┘ ┴
txt ───────┘ └┘ └┘ ┴
par ───────┘ └┘ └┘ ┴
pid ───────┘ └┘ └┘ ┴
st ──────────────────────┘└────────────────┘└─────────────────────────┘└──
213 exact calc
src └────┘ └
typ └────┘ └
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ───────────────
214 abs(r) * ∥x∥ * (abs(r) * ∥x∥) = (abs(r) * abs(r)) * (∥x∥ * ∥x∥) : by ring
id ┴ ┴ ┴ └─┘
src ─────┘ └┘ ┴┴ ┴┴┴┴ └┘ ┴ └┘ ┴ └┘ ┴└─┘ └─┘ ┴ ┴ ┴ └──┘ ┴└────
typ ─────┘ └┘ ┴┴ ┴┴┴┴ └┘ ┴ └┘ ┴ └┘ ┴└─┘ └─┘ ┴ ┴ ┴ └──┘ ┴└────
doc ─────┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴└────
txt ─────┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴└────
par ─────┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴└────
pid ─────┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └──┘ └─────
st ─────────────────────────────────────────────────────────────────────────┘└─────
215 ... = r * (r * (∥x∥ * ∥x∥)) : by { rw abs_mul_abs_self, ring },
id ┴ ┴ └──────────────┘
src ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └─┘└─┘└──────────────┘└┘└───┘┴
typ ─────┘└──┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └───┘ └─┘└─┘└──────────────┘└┘└───┘┴
doc ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └─┘└─┘ └┘└───┘┴
txt ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └─┘└─┘ └┘└───┘┴
par ─────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └─┘└─┘ └┘└───┘┴
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘ └──────┘
st ─────┘└──────────────────────────────┘└────────────────────┘└─────┘└┘└
216 exact inner_self_nonneg,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────┘└─
217 exact mul_nonneg (abs_nonneg _) (sqrt_nonneg _)
id └────────┘ └────────┘ └─────────┘
src └────┘└────────┘┴ └────────┘└──┘ └─────────┘└───
typ └────┘└────────┘┴ └────────┘└──┘ └─────────┘└───
doc └────┘ ┴ └──┘ └───
txt └────┘ ┴ └──┘ └───
par └────┘ ┴ └──┘ └───
pid ┴ ┴ └──┘ └─┘└
st ────────────────────────────────────────────────────
218 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
219
220 end norm
221
222 section orthogonal
223
224 open filter
225
226 /--
227 Existence of minimizers
228 Let `u` be a point in an inner product space, and let `K` be a nonempty complete convex subset.
229 Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
230 -/
231 theorem exists_norm_eq_infi_of_complete_convex {K : set α} (ne : K.nonempty) (h₁ : is_complete K)
id └─┘ ┴ ┴└───────┘ └─────────┘ ┴
src └─┘ └───────┘ └─────────┘
typ └─┘ ┴ ┴└───────┘ └─────────┘ ┴
doc └───────┘ └─────────┘
232 (h₂ : convex K) : ∀ u : α, ∃ v ∈ K, ∥u - v∥ = ⨅ w : K, ∥u - w∥ := assume u,
id └────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴
doc └────┘ ┴ ┴
233 begin
st └─────
234 let δ := ⨅ w : K, ∥u - w∥,
id ┴ ┴┴ ┴┴ ┴ ┴
src └───────┘┴└───┘ ┴┴┴ ┴┴┴ ┴
typ └───────┘┴└───┘┴┴┴┴┴┴┴┴ ┴
doc └───────┘┴└───┘ ┴┴ ┴ ┴
txt └───────┘ └───┘ ┴ ┴ ┴
par └───────┘ └───┘ ┴ ┴ ┴
pid └───┘┴└─┘ └───┘ ┴ ┴ ┴
st ──────────────────────────┘└─
235 letI : nonempty K := ne.to_subtype,
id └──────┘ ┴ └───────────┘
src └─────┘└──────┘┴ └──┘└───────────┘
typ └─────┘└──────┘┴┴└──┘└───────────┘
doc └─────┘ ┴ └──┘
txt └─────┘ ┴ └──┘
par └─────┘ ┴ └──┘
pid ┴└┘ ┴ └──┘
st ───────────────────────────────────┘└─
236 have zero_le_δ : 0 ≤ δ,
id ┴ ┴
src └─────────────────┘┴┴
typ └─────────────────┘┴┴┴
doc └─────────────────┘ ┴
txt └─────────────────┘ ┴
par └─────────────────┘ ┴
pid └────────────┘└───┘ ┴
st ───────────────────────┘└─
237 apply le_cinfi, intro, exact norm_nonneg _,
id └──────┘ └─────────┘
src └────┘└──────┘ └───┘ └────┘└─────────┘└┘
typ └────┘└──────┘ └───┘ └────┘└─────────┘└┘
doc └────┘└──────┘ └───┘ └────┘ └┘
txt └────┘ └───┘ └────┘ └┘
par └────┘ └───┘ └────┘ └┘
pid ┴ ┴ └┘
st ─────────────────┘└─────┘└───────────────────┘└─
238 have δ_le : ∀ w : K, δ ≤ ∥u - w∥,
id ┴ ┴ ┴
src └──────────┘ └───┘ ┴ ┴ ┴ ┴ ┴
typ └──────────┘ └───┘┴ ┴┴┴ ┴ ┴┴ ┴
doc └──────────┘ └───┘ ┴ ┴ ┴ ┴ ┴
txt └──────────┘ └───┘ ┴ ┴ ┴ ┴ ┴
par └──────────┘ └───┘ ┴ ┴ ┴ ┴ ┴
pid └───────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────┘└─
239 assume w, apply cinfi_le, use (0:ℝ), rintros _ ⟨_, rfl⟩, exact norm_nonneg _,
id └──────┘ └─────────┘
src └──────┘ └────┘└──────┘ └──┘ └┘ ┴ └────────────────┘ └────┘└─────────┘└┘
typ └──────┘ └────┘└──────┘ └──┘ └┘ ┴ └────────────────┘ └────┘└─────────┘└┘
doc └──────┘ └────┘└──────┘ └──┘ └┘ ┴ └────────────────┘ └────┘ └┘
txt └──────┘ └────┘ └──┘ └┘ ┴ └────────────────┘ └────┘ └┘
par └──────┘ └────┘ └──┘ └┘ ┴ └────────────────┘ └────┘ └┘
pid └──────┘ ┴ ┴ └┘ ┴ └─────────┘ ┴ └┘
st ───────────┘└──────────────┘└─────────┘└──────────────────┘└───────────────────┘└─
240 have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩,
id ┴ ┴ ┴ └──┘
src └───────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ └┘ ┴
typ └───────────┘ └───┘┴ ┴┴┴ ┴ ┴┴ ┴ └──┘ └─────┘└──┘┴ └┘ ┴
doc └───────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ └┘ ┴
txt └───────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ └┘ ┴
par └───────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ └┘ ┴
pid └────────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ └┘ ┴
st ───────────────────────────────────────────────────────────────┘└─
241 -- Step 1: since `δ` is the infimum, can find a sequence `w : ℕ → K` in `K`
st ──────────────────────────────────────────────────────────────────────────────
242 -- such that `∥u - w n∥ < δ + 1 / (n + 1)` (which implies `∥u - w n∥ --> δ`);
st ────────────────────────────────────────────────────────────────────────────────
243 -- maybe this should be a separate lemma
st ───────────────────────────────────────────
244 have exists_seq : ∃ w : ℕ → K, ∀ n, ∥u - w n∥ < δ + 1 / (n + 1),
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘┴└───┘ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴└─┘┴┴ ┴ └─┘
typ └────────────────┘┴└───┘ ┴┴┴┴┴┴ └┘ ┴ ┴┴ ┴ ┴ ┴┴┴┴┴┴└─┘┴┴ ┴ └─┘
doc └────────────────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘
txt └────────────────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘
par └────────────────┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘
pid └─────────────┘└─┘ └───┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘
st ────────────────────────────────────────────────────────────────┘└─
245 have hδ : ∀n:ℕ, δ < δ + 1 / (n + 1), from
id ┴
src └────────┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └────
typ └────────┘ └┘ ┴ ┴ ┴┴┴ └─┘ ┴ ┴ └─┘ └────
doc └────────┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └────
txt └────────┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └────
par └────────┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └────
pid └─────┘└─┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └────
st ──────────────────────────────────────┘└──────
246 λ n, lt_add_of_le_of_pos (le_refl _) nat.one_div_pos_of_nat,
id └─────────────────┘ └─────┘ └────────────────────┘
src ─────┘ └──┘└─────────────────┘┴ └─────┘└──┘└────────────────────┘
typ ─────┘ └──┘└─────────────────┘┴ └─────┘└──┘└────────────────────┘
doc ─────┘ └──┘ ┴ └──┘
txt ─────┘ └──┘ ┴ └──┘
par ─────┘ └──┘ ┴ └──┘
pid ─────┘ └──┘ ┴ └──┘
st ────────────────────────────────────────────────────────────────┘└─
247 have h := λ n, exists_lt_of_cinfi_lt (hδ n),
id └───────────────────┘ └┘
src └────────┘ └──┘└───────────────────┘┴ ┴ ┴
typ └────────┘ └──┘└───────────────────┘┴ └┘┴ ┴
doc └────────┘ └──┘└───────────────────┘┴ ┴ ┴
txt └────────┘ └──┘ ┴ ┴ ┴
par └────────┘ └──┘ ┴ ┴ ┴
pid └────┘┴└─┘ └──┘ ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─
248 let w : ℕ → K := λ n, classical.some (h n),
id ┴ └────────────┘ ┴
src └──────┘ ┴ ┴ └──┘ └──┘└────────────┘┴ ┴ ┴
typ └──────┘ ┴ ┴┴└──┘ └──┘└────────────┘┴ ┴┴ ┴
doc └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
txt └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
par └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
pid └───┘└─┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
st ─────────────────────────────────────────────┘└─
249 exact ⟨w, λ n, classical.some_spec (h n)⟩,
id ┴ └─────────────────┘ ┴
src └────┘ └┘ └──┘└─────────────────┘┴ ┴ └┘
typ └────┘ ┴└┘ └──┘└─────────────────┘┴ ┴┴ └┘
doc └────┘ └┘ └──┘ ┴ ┴ └┘
txt └────┘ └┘ └──┘ ┴ ┴ └┘
par └────┘ └┘ └──┘ ┴ ┴ └┘
pid ┴ └┘ └──┘ ┴ ┴ └┘
st ────────────────────────────────────────────┘└─
250 rcases exists_seq with ⟨w, hw⟩,
id └────────┘
src └─────┘ └───────────┘
typ └─────┘└────────┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ───────────────────────────────┘└─
251 have norm_tendsto : tendsto (λ n, ∥u - w n∥) at_top (𝓝 δ),
id └─────┘ ┴ ┴ └────┘ ┴ ┴
src └──────────────────┘└─────┘┴ └──┘ ┴ ┴ ┴ └┘└────┘┴ ┴┴ ┴
typ └──────────────────┘└─────┘┴ └──┘ ┴┴ ┴┴┴ └┘└────┘┴ ┴┴┴┴
doc └──────────────────┘└─────┘┴ └──┘ ┴ ┴ ┴ └┘└────┘┴ ┴┴ ┴
txt └──────────────────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └──────────────────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └───────────────┘└─┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘└─
252 have h : tendsto (λ n:ℕ, δ) at_top (𝓝 δ),
id └─────┘ └────┘ ┴
src └───────┘└─────┘┴ └─┘ └┘ └┘└────┘┴ ┴ ┴
typ └───────┘└─────┘┴ └─┘ └┘ └┘└────┘┴ ┴┴┴
doc └───────┘└─────┘┴ └─┘ └┘ └┘└────┘┴ ┴ ┴
txt └───────┘ ┴ └─┘ └┘ └┘ ┴ ┴ ┴
par └───────┘ ┴ └─┘ └┘ └┘ ┴ ┴ ┴
pid └────┘└─┘ ┴ └─┘ └┘ └┘ ┴ ┴ ┴
st ───────────────────────────────────────────┘└─
253 exact tendsto_const_nhds,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└─
254 have h' : tendsto (λ n:ℕ, δ + 1 / (n + 1)) at_top (𝓝 δ),
id └─────┘ └────┘ ┴
src └────────┘└─────┘┴ └─┘ └┘ ┴ └─┘ ┴ ┴ └───┘└────┘┴ ┴ ┴
typ └────────┘└─────┘┴ └─┘ └┘ ┴ └─┘ ┴ ┴ └───┘└────┘┴ ┴┴┴
doc └────────┘└─────┘┴ └─┘ └┘ ┴ └─┘ ┴ ┴ └───┘└────┘┴ ┴ ┴
txt └────────┘ ┴ └─┘ └┘ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴ ┴
par └────────┘ ┴ └─┘ └┘ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴ ┴
pid └─────┘└─┘ ┴ └─┘ └┘ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘└─
255 convert h.add tendsto_one_div_add_at_top_nhds_0_nat, simp only [add_zero],
id └───┘ └───────────────────────────────────┘ └──────┘
src └──────┘└───┘┴└───────────────────────────────────┘ └─────────┘└──────┘┴
typ └──────┘└───┘┴└───────────────────────────────────┘ └─────────┘└──────┘┴
doc └──────┘ ┴ └─────────┘ ┴
txt └──────┘ ┴ └─────────┘ ┴
par └──────┘ ┴ └─────────┘ ┴
pid ┴ ┴ ┴└──┘└┘ ┴
st ────────────────────────────────────────────────────────┘└────────────────────┘└─
256 exact tendsto_of_tendsto_of_tendsto_of_le_of_le h h'
id └───────────────────────────────────────┘ ┴ └┘
src └────┘└───────────────────────────────────────┘┴ ┴ └
typ └────┘└───────────────────────────────────────┘┴┴┴└┘└
doc └────┘└───────────────────────────────────────┘┴ ┴ └
txt └────┘ ┴ ┴ └
par └────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────
257 (filter.eventually_of_forall _ $ λ x, δ_le _)
id └──┘
src ─────┘ └─┘ ┴ └──┘ └───
typ ─────┘ └─┘ ┴ └──┘└──┘└───
doc ─────┘ └─┘ ┴ └──┘ └───
txt ─────┘ └─┘ ┴ └──┘ └───
par ─────┘ └─┘ ┴ └──┘ └───
pid ─────┘ └─┘ ┴ └──┘ └───
st ────────────────────────────────────────────────────
258 (filter.eventually_of_forall _ $ λ x, le_of_lt (hw _)),
id └─────────────────────────┘ └──────┘ └┘
src ─────┘ └─────────────────────────┘└─┘ ┴ └──┘└──────┘┴ └──┘
typ ─────┘ └─────────────────────────┘└─┘ ┴ └──┘└──────┘┴ └┘└──┘
doc ─────┘ └─┘ ┴ └──┘ ┴ └──┘
txt ─────┘ └─┘ ┴ └──┘ ┴ └──┘
par ─────┘ └─┘ ┴ └──┘ ┴ └──┘
pid ─────┘ └─┘ ┴ └──┘ ┴ └──┘
st ───────────────────────────────────────────────────────────┘└─
259 -- Step 2: Prove that the sequence `w : ℕ → K` is a Cauchy sequence
st ──────────────────────────────────────────────────────────────────────
260 have seq_is_cauchy : cauchy_seq (λ n, ((w n):α)),
id └────────┘ ┴ ┴
src └───────────────────┘└────────┘┴ └──┘ ┴ └┘ └┘
typ └───────────────────┘└────────┘┴ └──┘ ┴┴ └┘┴└┘
doc └───────────────────┘└────────┘┴ └──┘ ┴ └┘ └┘
txt └───────────────────┘ ┴ └──┘ ┴ └┘ └┘
par └───────────────────┘ ┴ └──┘ ┴ └┘ └┘
pid └────────────────┘└─┘ ┴ └──┘ ┴ └┘ └┘
st ─────────────────────────────────────────────────┘└─
261 rw cauchy_seq_iff_le_tendsto_0, -- splits into three goals
id └─────────────────────────┘
src └─┘└─────────────────────────┘
typ └─┘└─────────────────────────┘
doc └─┘└─────────────────────────┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────────────┘└────────────────────────────
262 let b := λ n:ℕ, (8 * δ * (1/(n+1)) + 4 * (1/(n+1)) * (1/(n+1))),
id ┴ ┴
src └───────┘ └─┘ └┘ └┘┴┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
typ └───────┘ └─┘ └┘ └┘┴┴┴┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
doc └───────┘ └─┘ └┘ └┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
txt └───────┘ └─┘ └┘ └┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
par └───────┘ └─┘ └┘ └┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
pid └───┘┴└─┘ └─┘ └┘ └┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └──┘
st ──────────────────────────────────────────────────────────────────┘└─
263 use (λn, sqrt (b n)),
id └──┘ ┴
src └──┘ └─┘└──┘┴ ┴ └┘
typ └──┘ └─┘└──┘┴ ┴┴ └┘
doc └──┘ └─┘ ┴ ┴ └┘
txt └──┘ └─┘ ┴ ┴ └┘
par └──┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ └┘
st ───────────────────────┘└─
264 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
265 -- first goal : `∀ (n : ℕ), 0 ≤ sqrt (b n)`
st ─────────────────────────────────────────────────
266 assume n, exact sqrt_nonneg _,
id └─────────┘
src └──────┘ └────┘└─────────┘└┘
typ └──────┘ └────┘└─────────┘└┘
doc └──────┘ └────┘ └┘
txt └──────┘ └────┘ └┘
par └──────┘ └────┘ └┘
pid └──────┘ ┴ └┘
st ───────────┘└───────────────────┘└─
267 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
268 -- second goal : `∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ sqrt (b N)`
st ──────────────────────────────────────────────────────────────────────────────────────
269 assume p q N hp hq,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └────────────────┘
st ─────────────────────┘└─
270 let wp := ((w p):α), let wq := ((w q):α),
id ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ └┘ ┴ └────────┘ ┴ └┘ ┴
typ └────────┘ ┴┴┴└┘┴┴ └────────┘ ┴┴┴└┘┴┴
doc └────────┘ ┴ └┘ ┴ └────────┘ ┴ └┘ ┴
txt └────────┘ ┴ └┘ ┴ └────────┘ ┴ └┘ ┴
par └────────┘ ┴ └┘ ┴ └────────┘ ┴ └┘ ┴
pid └────┘┴└─┘ ┴ └┘ ┴ └────┘┴└─┘ ┴ └┘ ┴
st ──────────────────────┘└───────────────────┘└─
271 let a := u - wq, let b := u - wp,
id ┴ └┘ ┴ └┘
src └───────┘ ┴ ┴ └───────┘ ┴ ┴
typ └───────┘┴┴ ┴└┘ └───────┘┴┴ ┴└┘
doc └───────┘ ┴ ┴ └───────┘ ┴ ┴
txt └───────┘ ┴ ┴ └───────┘ ┴ ┴
par └───────┘ ┴ ┴ └───────┘ ┴ ┴
pid └───┘┴└─┘ ┴ ┴ └───┘┴└─┘ ┴ ┴
st ──────────────────┘└───────────────┘└─
272 let half := 1 / (2:ℝ), let div := 1 / ((N:ℝ) + 1),
id ┴
src └────────────┘ ┴ └┘ ┴ └───────────┘ ┴ ┴ └┘ └─┘
typ └────────────┘ ┴ └┘ ┴ └───────────┘ ┴ ┴┴ └┘ └─┘
doc └────────────┘ ┴ └┘ ┴ └───────────┘ ┴ ┴ └┘ └─┘
txt └────────────┘ ┴ └┘ ┴ └───────────┘ ┴ ┴ └┘ └─┘
par └────────────┘ ┴ └┘ ┴ └───────────┘ ┴ ┴ └┘ └─┘
pid └──────┘┴└───┘ ┴ └┘ ┴ └─────┘┴└───┘ ┴ ┴ └┘ └─┘
st ────────────────────────┘└──────────────────────────┘└─
273 have : 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥ =
id ┴ ┴ └──┘ └┘ └┘ ┴
src └───────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴└
typ └───────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴└──┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴└┘ ┴┴└
doc └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid └───┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────────────────────────────────────
274 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) :=
id ┴ ┴
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───
st ─────────────────────────────────────
275 calc
src ───┘ └
typ ───┘ └
doc ───┘ └
txt ───┘ └
par ───┘ └
pid ───┘ └
st ─────────
276 4 * ∥u - half•(wq + wp)∥ * ∥u - half•(wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ──────────────────────────────────────────────────────────────────────────────
277 = (2*∥u - half•(wq + wp)∥) * (2 * ∥u - half•(wq + wp)∥) + ∥wp-wq∥*∥wp-wq∥ : by ring
id ┴ └──┘ └┘ └┘
src ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴└────
typ ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴┴ ┴└──┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘ └─┘ ┴└────
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴└────
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴└────
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴└────
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └─────
st ───────────────────────────────────────────────────────────────────────────────────────┘└─────
278 ... = (abs((2:ℝ)) * ∥u - half•(wq + wp)∥) * (abs((2:ℝ)) * ∥u - half•(wq+wp)∥) + ∥wp-wq∥*∥wp-wq∥ :
id └─┘
src ─────┘└──┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └──
typ ─────┘└──┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └──
doc ─────┘└──┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └──
txt ─────┘└──┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └──
par ─────┘└──┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └──
pid ─────────┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └──
st ─────┘└─────────────────────────────────────────────────────────────────────────────────────────────────
279 by { rw abs_of_nonneg, exact add_nonneg zero_le_one zero_le_one }
id └───────────┘ └────────┘ └─────────┘
src ─────┘ └─┘└─┘└───────────┘└┘└────┘└────────┘┴ ┴└─────────┘┴└─
typ ─────┘ └─┘└─┘└───────────┘└┘└────┘└────────┘┴ ┴└─────────┘┴└─
doc ─────┘ └─┘└─┘ └┘└────┘ ┴ ┴ ┴└─
txt ─────┘ └─┘└─┘ └┘└────┘ ┴ ┴ ┴└─
par ─────┘ └─┘└─┘ └┘└────┘ ┴ ┴ ┴└─
pid ─────┘ └────┘ └──────┘ ┴ ┴ └──
st ───────┘└─────────────────┘└─────────────────────────────────────────┘┴└
280 ... = ∥(2:ℝ) • (u - half • (wq + wp))∥ * ∥(2:ℝ) • (u - half • (wq + wp))∥ + ∥wp-wq∥ * ∥wp-wq∥ :
src ─────────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──
typ ─────────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──
doc ─────────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──
txt ─────────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──
par ─────────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──
pid ─────────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────────────────────────────────────────────────────────────
281 by { rw [norm_smul], refl }
id └───────┘
src ───────┘ └─┘└──┘└───────┘┴└┘└───┘└─
typ ───────┘ └─┘└──┘└───────┘┴└┘└───┘└─
doc ───────┘ └─┘└──┘ ┴└┘└───┘└─
txt ───────┘ └─┘└──┘ ┴└┘└───┘└─
par ───────┘ └─┘└──┘ ┴└┘└───┘└─
pid ───────┘ └─────┘ └─────────
st ─────────┘└──────────────┘└──────┘┴└
282 ... = ∥a + b∥ * ∥a + b∥ + ∥a - b∥ * ∥a - b∥ :
src ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
typ ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ────────────────────────────────────────────────────
283 begin
src ─────┘ └
typ ─────┘ └
doc ─────┘ └
txt ─────┘ └
par ─────┘ └
pid ─────┘ └
st ─────┘└─────
284 rw [smul_sub, smul_smul, mul_one_div_cancel two_ne_zero, ← one_add_one_eq_two, add_smul],
id └──────┘ └───────┘ └────────────────┘ └─────────┘ └────────────────┘ └──────┘
src ───────┘└──┘└──────┘└┘└───────┘└┘└────────────────┘┴└─────────┘└──┘└────────────────┘└┘└──────┘┴└─
typ ───────┘└──┘└──────┘└┘└───────┘└┘└────────────────┘┴└─────────┘└──┘└────────────────┘└┘└──────┘┴└─
doc ───────┘└──┘ └┘ └┘ ┴ └──┘ └┘ ┴└─
txt ───────┘└──┘ └┘ └┘ ┴ └──┘ └┘ ┴└─
par ───────┘└──┘ └┘ └┘ ┴ └──┘ └┘ ┴└─
pid ───────────┘ └┘ └┘ ┴ └──┘ └┘ └──
st ───────────────────┘└─────────┘└──────────────────────────────┘└────────────────────┘└────────┘└──
285 simp only [one_smul],
id └──────┘
src ───────┘└─────────┘└──────┘┴└─
typ ───────┘└─────────┘└──────┘┴└─
doc ───────┘└─────────┘ ┴└─
txt ───────┘└─────────┘ ┴└─
par ───────┘└─────────┘ ┴└─
pid ──────────────────┘ └──
st ───────────────────────────┘└─
286 have eq₁ : wp - wq = a - b, show wp - wq = (u - wq) - (u - wp), abel,
id └┘ └┘ ┴ ┴ └┘ ┴ └┘
src ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└┘└──┘└─
typ ──────────────────┘└┘┴ ┴└┘┴ ┴┴┴ ┴┴└┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴└┘└┘ ┴ ┴┴ ┴└┘┴└┘└──┘└─
doc ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└┘└──┘└─
txt ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└┘└──┘└─
par ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└┘└──┘└─
pid ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────────
st ─────────────────────────────────┘└──────────────────────────────────┘└────┘└─
287 have eq₂ : u + u - (wq + wp) = a + b, show u + u - (wq + wp) = (u - wq) + (u - wp), abel,
id ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘
src ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└┘└──┘└─
typ ──────────────────┘ ┴ ┴┴┴ ┴ └┘┴ ┴└┘└┘ ┴┴┴ ┴┴└┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└┘└┘ ┴ ┴┴ ┴└┘┴└┘└──┘└─
doc ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└┘└──┘└─
txt ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└┘└──┘└─
par ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└┘└──┘└─
pid ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────────
st ───────────────────────────────────────────┘└────────────────────────────────────────────┘└────┘└─
288 rw [eq₁, eq₂],
id └─┘ └─┘
src ───────┘└──┘ └┘ ┴└─
typ ───────┘└──┘└─┘└┘└─┘┴└─
doc ───────┘└──┘ └┘ ┴└─
txt ───────┘└──┘ └┘ ┴└─
par ───────┘└──┘ └┘ ┴└─
pid ───────────┘ └┘ └──
st ──────────────┘└───┘└──
289 end
src ──────────
typ ──────────
doc ──────────
txt ──────────
par ──────────
pid ──────────
st ────────┘└
290 ... = 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) : parallelogram_law_with_norm,
id ┴ ┴ └─────────────────────────┘
src ─────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└─────────────────────────┘
typ ─────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└─────────────────────────┘
doc ─────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
txt ─────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
par ─────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
pid ─────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
st ────────────────────────────────────────────────────────────────────┘└─
291 have eq : δ ≤ ∥u - half • (wq + wp)∥,
id ┴ ┴ └──┘ └┘ └┘
src └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────┘┴┴ ┴ ┴┴ ┴└──┘┴ ┴ └┘┴ ┴└┘┴
doc └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────┘└─
292 rw smul_add,
id └──────┘
src └─┘└──────┘
typ └─┘└──────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────┘└─
293 apply δ_le', apply h₂,
src └────┘ └────┘
typ └────┘ └────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st ────────────────┘└────────┘└─
294 repeat {exact subtype.mem _},
id └─────────┘
src └──────┘└────┘└─────────┘└┘┴
typ └──────┘└────┘└─────────┘└┘┴
doc └──────┘└────┘ └┘┴
txt └──────┘└────┘ └┘┴
par └──────┘└────┘ └┘┴
pid └──────┘ └─┘
st ───────────────┘└─────────────────┘└┘└
295 repeat {exact le_of_lt one_half_pos},
id └──────┘ └──────────┘
src └──────┘└────┘└──────┘┴└──────────┘┴
typ └──────┘└────┘└──────┘┴└──────────┘┴
doc └──────┘└────┘ ┴ ┴
txt └──────┘└────┘ ┴ ┴
par └──────┘└────┘ ┴ ┴
pid └──────┘ ┴ ┴
st ───────────────┘└─────────────────────────┘└┘└
296 exact add_halves 1,
id └────────┘
src └────┘└────────┘└┘
typ └────┘└────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ ┴┴
st ─────────────────────────┘└─
297 have eq₁ : 4 * δ * δ ≤ 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥,
id ┴ ┴ └──┘ └┘ └┘
src └───────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ ┴┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴└──┘┴ ┴ └┘┴ ┴└┘┴
doc └───────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └───────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └──────┘└───┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────┘
298 mono, mono, norm_num, apply mul_nonneg, norm_num, exact norm_nonneg _,
299 have eq₂ : ∥a∥ * ∥a∥ ≤ (δ + div) * (δ + div) :=
id ┴ ┴ └─┘
typ ┴ ┴ └─┘
300 mul_self_le_mul_self (norm_nonneg _)
301 (le_trans (le_of_lt $ hw q) (add_le_add_left (nat.one_div_le_one_div hq) _)),
id ┴ └┘
typ ┴ └┘
302 have eq₂' : ∥b∥ * ∥b∥ ≤ (δ + div) * (δ + div) :=
id ┴ ┴ └─┘
typ ┴ ┴ └─┘
303 mul_self_le_mul_self (norm_nonneg _)
304 (le_trans (le_of_lt $ hw p) (add_le_add_left (nat.one_div_le_one_div hp) _)),
id ┴ └┘
typ ┴ └┘
305 rw dist_eq_norm,
306 apply nonneg_le_nonneg_of_squares_le, { exact sqrt_nonneg _ },
st └┘
307 rw mul_self_sqrt,
308 exact calc
309 ∥wp - wq∥ * ∥wp - wq∥ = 2 * (∥a∥*∥a∥ + ∥b∥*∥b∥) - 4 * ∥u - half • (wq+wp)∥ * ∥u - half • (wq+wp)∥ :
id ┴ ┴ ┴ └──┘ └┘ └┘
typ ┴ ┴ ┴ └──┘ └┘ └┘
310 by { rw ← this, simp }
st └┘
311 ... ≤ 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) - 4 * δ * δ : sub_le_sub_left eq₁ _
id ┴
typ ┴
312 ... ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ :
313 sub_le_sub_right (mul_le_mul_of_nonneg_left (add_le_add eq₂ eq₂') (by norm_num)) _
314 ... = 8 * δ * div + 4 * div * div : by ring,
id └─┘
typ └─┘
315 exact add_nonneg (mul_nonneg (mul_nonneg (by norm_num) zero_le_δ) (le_of_lt nat.one_div_pos_of_nat))
316 (mul_nonneg (mul_nonneg (by norm_num) (le_of_lt nat.one_div_pos_of_nat)) (le_of_lt nat.one_div_pos_of_nat)),
317 -- third goal : `tendsto (λ (n : ℕ), sqrt (b n)) at_top (𝓝 0)`
318 apply tendsto.comp,
319 { convert continuous_sqrt.continuous_at, exact sqrt_zero.symm },
st └┘
320 have eq₁ : tendsto (λ (n : ℕ), 8 * δ * (1 / (n + 1))) at_top (𝓝 (0:ℝ)),
id ┴
typ ┴
321 convert (@tendsto_const_nhds _ _ _ (8 * δ) _).mul tendsto_one_div_add_at_top_nhds_0_nat,
id ┴
typ ┴
322 simp only [mul_zero],
323 have : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1))) at_top (𝓝 (0:ℝ)),
324 convert (@tendsto_const_nhds _ _ _ (4:ℝ) _).mul tendsto_one_div_add_at_top_nhds_0_nat,
325 simp only [mul_zero],
326 have eq₂ : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1)) * (1 / (n + 1))) at_top (𝓝 (0:ℝ)),
327 convert this.mul tendsto_one_div_add_at_top_nhds_0_nat,
328 simp only [mul_zero],
329 convert eq₁.add eq₂, simp only [add_zero],
330 -- Step 3: By completeness of `K`, let `w : ℕ → K` converge to some `v : K`.
331 -- Prove that it satisfies all requirements.
332 rcases cauchy_seq_tendsto_of_is_complete h₁ (λ n, _) seq_is_cauchy with ⟨v, hv, w_tendsto⟩,
id ┴
typ ┴
333 use v, use hv,
id ┴
typ ┴
334 have h_cont : continuous (λ v, ∥u - v∥) :=
id ┴ ┴
typ ┴ ┴
335 continuous.comp continuous_norm (continuous.sub continuous_const continuous_id),
336 have : tendsto (λ n, ∥u - w n∥) at_top (𝓝 ∥u - v∥),
id ┴ ┴ ┴
typ ┴ ┴ ┴
337 convert (tendsto.comp h_cont.continuous_at w_tendsto),
338 exact tendsto_nhds_unique at_top_ne_bot this norm_tendsto,
339 exact subtype.mem _
340 end
st └─┘
341
342 /-- Characterization of minimizers in the above theorem -/
343 theorem norm_eq_infi_iff_inner_le_zero {K : set α} (h : convex K) {u : α} {v : α}
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
344 (hv : v ∈ K) : ∥u - v∥ = (⨅ w : K, ∥u - w∥) ↔ ∀ w ∈ K, inner (u - v) (w - v) ≤ 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
345 iff.intro
346 begin
347 assume eq w hw,
348 let δ := ⨅ w : K, ∥u - w∥, let p := inner (u - v) (w - v), let q := ∥w - v∥^2,
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
349 letI : nonempty K := ⟨⟨v, hv⟩⟩,
id └──────┘ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴
350 have zero_le_δ : 0 ≤ δ,
id ┴
typ ┴
351 apply le_cinfi, intro, exact norm_nonneg _,
352 have δ_le : ∀ w : K, δ ≤ ∥u - w∥,
id ┴ ┴
typ ┴ ┴
353 assume w, apply cinfi_le, use (0:ℝ), rintros _ ⟨_, rfl⟩, exact norm_nonneg _,
354 have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
355 have : ∀θ:ℝ, 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q,
id ┴ ┴
typ ┴ ┴
356 assume θ hθ₁ hθ₂,
357 have : ∥u - v∥^2 ≤ ∥u - v∥^2 - 2 * θ * inner (u - v) (w - v) + θ*θ*∥w - v∥^2 :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
358 calc
359 ∥u - v∥^2 ≤ ∥u - (θ•w + (1-θ)•v)∥^2 :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
360 begin
361 simp only [pow_two], apply mul_self_le_mul_self (norm_nonneg _),
362 rw [eq], apply δ_le',
363 apply h hw hv,
364 exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _],
365 end
st └─┘
366 ... = ∥(u - v) - θ • (w - v)∥^2 :
367 begin
368 have : u - (θ•w + (1-θ)•v) = (u - v) - θ • (w - v),
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
369 rw [smul_sub, sub_smul, one_smul], simp,
370 rw this
371 end
st └─┘
372 ... = ∥u - v∥^2 - 2 * θ * inner (u - v) (w - v) + θ*θ*∥w - v∥^2 :
373 begin
374 rw [norm_sub_pow_two, inner_smul_right, norm_smul],
375 simp only [pow_two],
376 show ∥u-v∥*∥u-v∥-2*(θ*inner(u-v)(w-v))+abs(θ)*∥w-v∥*(abs(θ)*∥w-v∥)=
377 ∥u-v∥*∥u-v∥-2*θ*inner(u-v)(w-v)+θ*θ*(∥w-v∥*∥w-v∥),
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
378 rw abs_of_pos hθ₁, ring
379 end,
st └─┘
380 have eq₁ : ∥u-v∥^2-2*θ*inner(u-v)(w-v)+θ*θ*∥w-v∥^2=∥u-v∥^2+(θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)), abel,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
381 rw [eq₁, le_add_iff_nonneg_right] at this,
382 have eq₂ : θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)=θ*(θ*∥w-v∥^2-2*inner(u-v)(w-v)), ring,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
383 rw eq₂ at this,
384 have := le_of_sub_nonneg (nonneg_of_mul_nonneg_left this hθ₁),
385 exact this,
386 by_cases hq : q = 0,
id ┴
typ ┴
387 { rw hq at this,
388 have : p ≤ 0,
id ┴
typ ┴
389 have := this (1:ℝ) (by norm_num) (by norm_num),
390 linarith,
391 exact this },
st └┘
392 { have q_pos : 0 < q,
id ┴
typ ┴
393 apply lt_of_le_of_ne, exact pow_two_nonneg _, intro h, exact hq h.symm,
394 by_contradiction hp, rw not_le at hp,
395 let θ := min (1:ℝ) (p / q),
id ┴ ┴
typ ┴ ┴
396 have eq₁ : θ*q ≤ p := calc
id ┴ ┴ ┴
typ ┴ ┴ ┴
397 θ*q ≤ (p/q) * q : mul_le_mul_of_nonneg_right (min_le_right _ _) (pow_two_nonneg _)
id ┴ ┴
typ ┴ ┴
398 ... = p : div_mul_cancel _ hq,
id ┴
typ ┴
399 have : 2 * p ≤ p := calc
id ┴
typ ┴
400 2 * p ≤ θ*q : by { refine this θ (lt_min (by norm_num) (div_pos hp q_pos)) (by norm_num) }
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
401 ... ≤ p : eq₁,
id ┴
typ ┴
402 linarith }
st └─
403 end
st ──┘
404 begin
405 assume h,
406 letI : nonempty K := ⟨⟨v, hv⟩⟩,
id └──────┘ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴
407 apply le_antisymm,
408 { apply le_cinfi, assume w,
409 apply nonneg_le_nonneg_of_squares_le (norm_nonneg _),
410 have := h w w.2,
411 exact calc
412 ∥u - v∥ * ∥u - v∥ ≤ ∥u - v∥ * ∥u - v∥ - 2 * inner (u - v) ((w:α) - v) : by linarith
id ┴ ┴ ┴
typ ┴ ┴ ┴
413 ... ≤ ∥u - v∥^2 - 2 * inner (u - v) ((w:α) - v) + ∥(w:α) - v∥^2 :
414 by { rw pow_two, refine le_add_of_nonneg_right _, exact pow_two_nonneg _ }
st └┘
415 ... = ∥(u - v) - (w - v)∥^2 : norm_sub_pow_two.symm
416 ... = ∥u - w∥ * ∥u - w∥ :
417 by { have : (u - v) - (w - v) = u - w, abel, rw [this, pow_two] } },
id ┴ ┴
typ ┴ ┴
st ┴ └──┘
418 { show (⨅ (w : K), ∥u - w∥) ≤ (λw:K, ∥u - w∥) ⟨v, hv⟩,
id ┴ ┴
typ ┴ ┴
419 apply cinfi_le, use 0, rintros y ⟨z, rfl⟩, exact norm_nonneg _ }
st └─
420 end
st ──┘
421
422 /--
423 Existence of minimizers.
424 Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace.
425 Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
426 This point `v` is usually called the orthogonal projection of `u` onto `K`.
427 -/
428 theorem exists_norm_eq_infi_of_complete_subspace (K : subspace ℝ α)
id ┴ ┴
src ┴
typ ┴ ┴
429 (h : is_complete (↑K : set α)) : ∀ u : α, ∃ v ∈ K, ∥u - v∥ = ⨅ w : (↑K : set α), ∥u - w∥ :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
430 exists_norm_eq_infi_of_complete_convex ⟨0, K.zero⟩ h K.convex
431
432 /--
433 Characterization of minimizers in the above theorem.
434 Let `u` be a point in an inner product space, and let `K` be a nonempty subspace.
435 Then point `v` minimizes the distance `∥u - v∥` if and only if
436 for all `w ∈ K`, `inner (u - v) w = 0` (i.e., `u - v` is orthogonal to the subspace `K`)
437 -/
438 theorem norm_eq_infi_iff_inner_eq_zero (K : subspace ℝ α) {u : α} {v : α}
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
439 (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set α), ∥u - w∥) ↔ ∀ w ∈ K, inner (u - v) w = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
440 iff.intro
441 begin
442 assume h,
443 have h : ∀ w ∈ K, inner (u - v) (w - v) ≤ 0,
id ┴ ┴
typ ┴ ┴
444 { rwa [norm_eq_infi_iff_inner_le_zero] at h, exacts [K.convex, hv] },
st └┘
445 assume w hw,
446 have le : inner (u - v) w ≤ 0,
id ┴ ┴ ┴
typ ┴ ┴ ┴
447 let w' := w + v,
id ┴ ┴
typ ┴ ┴
448 have : w' ∈ K := submodule.add_mem _ hw hv,
id └┘
typ └┘
449 have h₁ := h w' this,
id └┘
typ └┘
450 have h₂ : w' - v = w, simp only [add_neg_cancel_right, sub_eq_add_neg],
id └┘ ┴ ┴
typ └┘ ┴ ┴
451 rw h₂ at h₁, exact h₁,
452 have ge : inner (u - v) w ≥ 0,
id ┴ ┴ ┴
typ ┴ ┴ ┴
453 let w'' := -w + v,
id ┴ ┴
typ ┴ ┴
454 have : w'' ∈ K := submodule.add_mem _ (submodule.neg_mem _ hw) hv,
id └─┘
typ └─┘
455 have h₁ := h w'' this,
id └─┘
typ └─┘
456 have h₂ : w'' - v = -w, simp only [neg_inj', add_neg_cancel_right, sub_eq_add_neg],
id └─┘ ┴ ┴
typ └─┘ ┴ ┴
457 rw [h₂, inner_neg_right] at h₁,
458 linarith,
459 exact le_antisymm le ge
460 end
st └─┘
461 begin
462 assume h,
463 have : ∀ w ∈ K, inner (u - v) (w - v) ≤ 0,
id ┴ ┴ ┴
typ ┴ ┴ ┴
464 assume w hw,
465 let w' := w - v,
id ┴ ┴
typ ┴ ┴
466 have : w' ∈ K := submodule.sub_mem _ hw hv,
id └┘
typ └┘
467 have h₁ := h w' this,
id └┘
typ └┘
468 exact le_of_eq h₁,
469 rwa norm_eq_infi_iff_inner_le_zero,
470 exacts [submodule.convex _, hv]
471 end
st └─┘
472
473 end orthogonal